d-chooser(D;dec)
== j, b:Id, s:M(j).state.
== (isl(dec(j,b,s))  b in dom(M(j).pre) & (v:M(j).da(locl(b)). M(j).pre(b,s,v)))
== & (isl(dec(j,b,s))  b in dom(M(j).pre) & M(j).pre(b,s,outl(dec(j,b,s)))) 

latex

---

clarification:

d-chooser(D;dec)
== j:Id, b:Id, s:d-m(D; j).state.
== (isl(dec(j,b,s))  b in dom(d-m(D; j).pre) & (v:d-m(D; j).da(locl(b)). d-m(D; j).pre(b,s,v)))
== & (isl(dec(j,b,s))  b in dom(d-m(D; j).pre) & d-m(D; j).pre(b,s,outl(dec(j,b,s)))) 

latex

Definitions	Id, x:A. B(x), M.state, P & Q, P  Q, x:A. B(x), M.da(a), locl(a), P  Q, b, isl(x), A & B, a in dom(M.pre), M.pre(a,s,v), M(i), outl(x), f(a)
FDL editor aliases	d-chooser